/*
Copyright 2007 Nicola Olivetti, Gian Luca Pozzato
This file is part of CondLean.
CondLean is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
CondLean is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with CondLean. If not, see .
*/
/* Theorem prover SeqCS: free variable version */
/* Labels are integer starting with 1 */
:- op(400,fy,neg),
op(500,xfy,and),
op(600,xfy,or),
op(650,xfy,->),
op(650,xfy,=>).
:-use_module(library(lists)).
:-use_module(library(clpfd)).
/* --------------------------------------------------------------------------------------- */
/* Axioms */
/* true and false */
prove(_,_,[LitSigma,_,_],_,_,tree(falso),Free,Free):-
member([_,false],LitSigma),!.
prove(_,_,_,[LitDelta,_,_],_,tree(vero),Free,Free):-
member([_,true],LitDelta),!.
prove(_,_,[LitSigma,_,_],[LitDelta,_,_],_,tree(assioma),Free,Free):-
member([X,F],LitSigma),member([Y,F],LitDelta),X==Y.
prove(_,_,[_,TransSigma,_],[_,TransDelta,_],_,tree(assioma),Free,Free):-
member([X,F,Y],TransSigma),member([U,F,V],TransDelta),X==U,Y==V.
prove(_,_,[_,_,ComplexSigma],[_,_,ComplexDelta],_,tree(assioma),Free,Free):-
member([X,F],ComplexSigma),member([Y,F],ComplexDelta),X==Y.
prove(_,_,[LitSigma,_,_],[LitDelta,_,_],_,tree(assioma),Free,Free):-
member(F,LitSigma),member(F,LitDelta).
prove(_,_,[_,TransSigma,_],[_,TransDelta,_],_,tree(assioma),Free,Free):-
member(F,TransSigma),member(F,TransDelta).
prove(_,_,[_,_,ComplexSigma],[_,_,ComplexDelta],_,tree(assioma),Free,Free):-
member(F,ComplexSigma),member(F,ComplexDelta).
/* Rules */
/* and L */
prove(CS,Cond,[LitSigma,TransSigma,ComplexSigma],Delta,Max,
tree(andL,ProofTail,[X,A and B]),Free,NewFree):-
select([X,A and B],ComplexSigma,ResComplexSigma),!,
put([X,A],LitSigma,ResComplexSigma,TempLitSigma,TempComplexSigma),
put([X,B],TempLitSigma,TempComplexSigma,NewLitSigma,NewComplexSigma),
prove(CS,Cond,[NewLitSigma,TransSigma,NewComplexSigma],Delta,Max,ProofTail,Free,NewFree).
/* or R */
prove(CS,Cond,Sigma,[LitDelta,TransDelta,ComplexDelta],Max,
tree(orR,ProofTail,[X,A or B]),Free,NewFree):-
select([X,A or B],ComplexDelta,ResComplexDelta),!,
put([X,A],LitDelta,ResComplexDelta,TempLitDelta,TempComplexDelta),
put([X,B],TempLitDelta,TempComplexDelta,NewLitDelta,NewComplexDelta),
prove(CS,Cond,Sigma,[NewLitDelta,TransDelta,NewComplexDelta],Max,ProofTail,Free,NewFree).
/* neg R */
prove(CS,Cond,[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta],
Max,tree(negR,ProofTail,[X,neg A]),Free,NewFree):-
select([X,neg A],ComplexDelta,ResComplexDelta),!,
put([X,A],LitSigma,ComplexSigma,NewLitSigma,NewComplexSigma),
prove(CS,Cond,[NewLitSigma,TransSigma,NewComplexSigma],[LitDelta,TransDelta,ResComplexDelta],Max,
ProofTail,Free,NewFree).
/* neg L */
prove(CS,Cond,[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta],Max,
tree(negL,ProofTail,[X,neg A]),Free,NewFree)
:-select([X,neg A],ComplexSigma,ResComplexSigma),!,
put([X,A],LitDelta,ComplexDelta,NewLitDelta,NewComplexDelta),
prove(CS,Cond,[LitSigma,TransSigma,ResComplexSigma],[NewLitDelta,TransDelta,NewComplexDelta],Max,
ProofTail,Free,NewFree).
/* -> R */
prove(CS,Cond,[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta],Max,
tree(impR,ProofTail,[X,A -> B]),Free,NewFree)
:-select([X,A -> B],ComplexDelta,ResComplexDelta),!,
put([X,A],LitSigma,ComplexSigma,NewLitSigma,NewComplexSigma),
put([X,B],LitDelta,ResComplexDelta,NewLitDelta,NewComplexDelta),
prove(CS,Cond,[NewLitSigma,TransSigma,NewComplexSigma],[NewLitDelta,TransDelta,NewComplexDelta],Max,
ProofTail,Free,NewFree).
/* => R */
prove(CS,Cond,[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta],Max,
tree(condR,ProofTail,Y,[X,A => B]),Free,NewFree)
:-select([X,A => B],ComplexDelta,ResComplexDelta),!,
Y#=Max+1,
put([Y,B],LitDelta,ResComplexDelta,NewLitDelta,NewComplexDelta),
prove(CS,Cond,[LitSigma,[[X,A,Y]|TransSigma],ComplexSigma],[NewLitDelta,TransDelta,NewComplexDelta],
Y,ProofTail,Free,NewFree).
/* and R */
prove(CS,Cond,Sigma,[LitDelta,TransDelta,ComplexDelta],Max,
tree(andR,LeftProof,RightProof,[X,A and B]),Free,NewFree):-
select([X,A and B],ComplexDelta,ResComplexDelta),!,
put([X,A],LitDelta,ResComplexDelta,FirstLitDelta,FirstComplexDelta),
put([X,B],LitDelta,ResComplexDelta,SecLitDelta,SecComplexDelta),
prove(CS,Cond,Sigma,[FirstLitDelta,TransDelta,FirstComplexDelta],Max,LeftProof,Free,TempFree),
prove(CS,Cond,Sigma,[SecLitDelta,TransDelta,SecComplexDelta],Max,RightProof,TempFree,NewFree).
/* or L */
prove(CS,Cond,[LitSigma,TransSigma,ComplexSigma],Delta,Max,
tree(orL,LeftProof,RightProof,[X,A or B]),Free,NewFree):-
select([X,A or B],ComplexSigma,ResComplexSigma),!,
put([X,A],LitSigma,ResComplexSigma,FirstLitSigma,FirstComplexSigma),
put([X,B],LitSigma,ResComplexSigma,SecLitSigma,SecComplexSigma),
prove(CS,Cond,[FirstLitSigma,TransSigma,FirstComplexSigma],Delta,Max,LeftProof,Free,TempFree),
prove(CS,Cond,[SecLitSigma,TransSigma,SecComplexSigma],Delta,Max,RightProof,TempFree,NewFree).
/* -> L */
prove(CS,Cond,[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta],Max,
tree(impL,LeftTail,RightTail,[X,A -> B]),Free,NewFree):-
select([X,A -> B],ComplexSigma,ResComplexSigma),!,
put([X,A],LitDelta,ComplexDelta,NewLitDelta,NewComplexDelta),
put([X,B],LitSigma,ResComplexSigma,NewLitSigma,NewComplexSigma),
prove(CS,Cond,[LitSigma,TransSigma,ResComplexSigma],[NewLitDelta,TransDelta,NewComplexDelta],
Max,LeftTail,Free,TempFree),
prove(CS,Cond,[NewLitSigma,TransSigma,NewComplexSigma],[LitDelta,TransDelta,ComplexDelta],
Max,RightTail,TempFree,NewFree).
/* CS */
prove(CS,Cond,[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta],Max,
tree(cs,LeftProof,RightProof,U,[X,A,Y]),Free,NewFree):-
member([X,A,Y],TransSigma),
X\=Y,
\+member([X,A,Y],CS),!,
put([X,A],LitDelta,ComplexDelta,NewLitDelta,NewComplexDelta),
prove([[X,A,Y]|CS],Cond,[LitSigma,TransSigma,ComplexSigma],[NewLitDelta,TransDelta,NewComplexDelta],Max,LeftProof,Free,TempFree),
U#=Max+1,
labelSubstitution(LitSigma,X,U,TempLitSigma),
labelSubstitution(TempLitSigma,Y,U,DefLitSigma),
labelSubstitution(TransSigma,X,U,TempTransSigma),
labelSubstitution(TempTransSigma,Y,U,DefTransSigma),
labelSubstitution(ComplexSigma,X,U,TempComplexSigma),
labelSubstitution(TempComplexSigma,Y,U,DefComplexSigma),
labelSubstitution(LitDelta,X,U,TempLitDelta),
labelSubstitution(TempLitDelta,Y,U,DefLitDelta),
labelSubstitution(TransDelta,X,U,TempTransDelta),
labelSubstitution(TempTransDelta,Y,U,DefTransDelta),
labelSubstitution(ComplexDelta,X,U,TempComplexDelta),
labelSubstitution(TempComplexDelta,Y,U,DefComplexDelta),
prove(CS,Cond,[DefLitSigma,DefTransSigma,DefComplexSigma],
[DefLitDelta,DefTransDelta,DefComplexDelta],U,RightProof,TempFree,NewFree).
/* => L */
prove(CS,Cond,[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta],Max,tree(condL,LeftTail,RightTail,Y,[X,A => B]),
Free,NewFree):-
member([X,A => B],ComplexSigma),
\+member([[X,A => B],_,_],Cond),
y_domain(X,TransSigma,YDomain),
list_to_fdset(YDomain,Y_FD_Domain),
Y in_set Y_FD_Domain,
put([Y,B],LitSigma,ComplexSigma,NewLitSigma,NewComplexSigma),
prove(CS,[[[X,A => B],[Y],ok]|Cond],[NewLitSigma,TransSigma,NewComplexSigma],[LitDelta,TransDelta,ComplexDelta],
Max,LeftTail,[Y|Free],TempFree),
prove(CS,[[[X,A => B],[Y],ok]|Cond],[LitSigma,TransSigma,ComplexSigma],[LitDelta,[[X,A,Y]|TransDelta],ComplexDelta],Max,
RightTail,TempFree,NewFree).
/* => L */
prove(CS,Cond,[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta],Max,tree(condL,LeftTail,RightTail,Y,[X,A => B]),
Free,NewFree):-
member([X,A => B],ComplexSigma),
select([[X,A => B],UsedVariables,LabellingStatus],Cond,NewCond),
y_domain(X,TransSigma,TempYDomain),
length(TempYDomain,AvailableLabels),
length(UsedVariables,NumUsedVariables),
NumUsedVariables B],[Y|UsedVariables],LabellingStatus]|NewCond],[NewLitSigma,TransSigma,NewComplexSigma],[LitDelta,TransDelta,ComplexDelta],
Max,LeftTail,[Y|Free],TempFree),
prove(CS,[[[X,A => B],[Y|UsedVariables],LabellingStatus]|NewCond],[LitSigma,TransSigma,ComplexSigma],[LitDelta,[[X,A,Y]|TransDelta],ComplexDelta],Max,
RightTail,TempFree,NewFree).
/* => L */
prove(CS,Cond,[LitSigma,TransSigma,ComplexSigma],Delta,Max,SubTree,Free,NewFree):-
member([X,A => B],ComplexSigma),
select([[X,A => B],UsedVariables,ok],Cond,NewCond),
labeling([],UsedVariables),
prove(CS,[[[X,A => B],UsedVariables,stop]|NewCond],[LitSigma,TransSigma,ComplexSigma],Delta,Max,SubTree,Free,NewFree).
/* EQ */
prove(_,_,[_,TransSigma,_],[_,TransDelta,_],_,tree(eq,LeftProof,RightProof,[X,A,Y],[X,B,Y]),
Free,Free):-
member([X,A,Y],TransSigma),member([X,B,Y],TransDelta),
/* The premises are "independent" from the conclusion, so we can use label 1
for their proofs */
put([1,A],[],[],FirstLitSigma,FirstComplexSigma),
put([1,B],[],[],FirstLitDelta,FirstComplexDelta),
put([1,B],[],[],SecLitSigma,SecComplexSigma),
put([1,A],[],[],SecLitDelta,SecComplexDelta),
prove([],[],[FirstLitSigma,[],FirstComplexSigma],[FirstLitDelta,[],FirstComplexDelta],
1,LeftProof,[],Temp1Free),
prove([],[],[SecLitSigma,[],SecComplexSigma],[SecLitDelta,[],SecComplexDelta],
1,RightProof,[],Temp2Free),
labeling([],Temp1Free),labeling([],Temp2Free).
/* --------------------------------------------------------------------------------------- */
/* Given a label (constant or variable) X and the list of transitions Trans, this predicate
extracts all the transitions in Trans of the form [X,C,W], then W is added to the list
corresponding to the domain of the free variable Y introduced (backward) by the (=> L) rule */
y_domain(_,[],[]):-!.
y_domain(X,[[X,_,W]|Tail],[W|ResTail]):-!,y_domain(X,Tail,ResTail).
y_domain(X,[_|Tail],ResTail):-!,y_domain(X,Tail,ResTail).
/* --------------------------------------------------------------------------------------- */
/* Auxiliary predicate for the (CS) and (CEM) rules */
labelSubstitution([],_,_,[]):-!.
labelSubstitution([[X,F]|Tail],X,U,[[U,F]|ResTail]):-labelSubstitution(Tail,X,U,ResTail).
labelSubstitution([[X,F,X]|Tail],X,U,[[U,F,U]|ResTail]):-labelSubstitution(Tail,X,U,ResTail).
labelSubstitution([[X,F,Y]|Tail],X,U,[[U,F,Y]|ResTail]):-X#\=Y,labelSubstitution(Tail,X,U,ResTail).
labelSubstitution([[Y,F,X]|Tail],X,U,[[Y,F,U]|ResTail]):-X#\=Y,labelSubstitution(Tail,X,U,ResTail).
labelSubstitution([[Y,F,Z]|Tail],X,U,[[Y,F,Z]|ResTail]):-X#\=Y,X#\=Z,labelSubstitution(Tail,X,U,ResTail).
labelSubstitution([[Y,F]|Tail],X,U,[[Y,F]|ResTail]):-Y#\=X,labelSubstitution(Tail,X,U,ResTail).
/* --------------------------------------------------------------------------------------- */
/* This predicate creates a partition of the sequent in atomic, transition and complex formulas */
struttura([],[],[],[]):-!.
struttura([[X,A and B]|Tail],Literal,Transaction,[[X,A and B]|ForTail]):-
struttura(Tail,Literal,Transaction,ForTail),!.
struttura([[X,A or B]|Tail],Literal,Transaction,[[X,A or B]|ForTail]):-
struttura(Tail,Literal,Transaction,ForTail),!.
struttura([[X,A -> B]|Tail],Literal,Transaction,[[X,A -> B]|ForTail]):-
struttura(Tail,Literal,Transaction,ForTail),!.
struttura([[X,A => B]|Tail],Literal,Transaction,[[X,A => B]|ForTail]):-
struttura(Tail,Literal,Transaction,ForTail),!.
struttura([[X,neg A]|Tail],Literal,Transaction,[[X,neg A]|ForTail]):-
struttura(Tail,Literal,Transaction,ForTail),!.
struttura([[X,A,Y]|Tail],Literal,[[X,A,Y]|TransTail],Formulae):-
struttura(Tail,Literal,TransTail,Formulae),!.
struttura([X|Tail],[X|LitTail],Transition,Formulae):-
struttura(Tail,LitTail,Transition,Formulae),!.
/* This predicate inserts a formula in the correct list; more precisely, a formula
can be an atomic formula or a complex formula */
put([X,A and B],Literal,Formulae,Literal,[[X,A and B]|Formulae]):-!.
put([X,A or B],Literal,Formulae,Literal,[[X,A or B]|Formulae]):-!.
put([X,A -> B],Literal,Formulae,Literal,[[X,A -> B]|Formulae]):-!.
put([X,A => B],Literal,Formulae,Literal,[[X,A => B]|Formulae]):-!.
put([X,neg A],Literal,Formulae,Literal,[[X,neg A]|Formulae]):-!.
put(X,Literal,Formulae,[X|Literal],Formulae):-!.
/* --------------------------------------------------------------------------------------- */
/* All the following predicates are used to link the SICStus Prolog implementation to the
graphical interface */
/* --------------------------------------------------------------------------------------- */
/* This predicate is invoked from the graphical interface (Java) */
proof(Sigma,Delta,JavaProof,LunghSeq,GradoSeq,NumEtichette,Altezza,NumNodi,
NumCondR,NumCondL,NumEq,NumContr):-
struttura(Sigma,LitSigma,TransSigma,ForSigma),
struttura(Delta,LitDelta,TransDelta,ForDelta),
prove([],[],[LitSigma,TransSigma,ForSigma],[LitDelta,TransDelta,ForDelta],1,ProofTree,[],NewTree),
labeling([],NewTree),
costruisciJava(ProofTree,[[LitSigma,TransSigma,ForSigma],[LitDelta,TransDelta,ForDelta]]
,JavaProof),
lunghezzaSequente(Sigma,LSigma),lunghezzaSequente(Delta,LDelta),LunghSeq is LSigma+LDelta,
gradoSequente(ForSigma,GSigma),gradoSequente(ForDelta,GDelta),GradoSeq is GSigma+GDelta,
etichetteUsate(JavaProof,NumEtichette),
altezzaAlbero(JavaProof,Altezza),
nodiAlbero(JavaProof,NumNodi),
condADestra(JavaProof,NumCondR),
condASinistra(JavaProof,NumCondL),
eqPresenti(JavaProof,NumEq),
contrazioni(JavaProof,NumContr).
/* --------------------------------------------------------------------------------------- */
/* Statistics */
contrazioni(_,0).
eqPresenti(null,0).
eqPresenti(new_Tree(_,eq,_,_,_,LeftProof,RightProof),NumEq):-!,
eqPresenti(LeftProof,EqL),eqPresenti(RightProof,EqR),NumEq is 1+EqL+EqR.
eqPresenti(new_Tree(_,_,_,_,_,LeftProof,RightProof),NumEq):-
eqPresenti(LeftProof,EqL),eqPresenti(RightProof,EqR),NumEq is EqL+EqR.
condADestra(null,0).
condADestra(new_Tree(_,condR,_,_,_,LeftProof,RightProof),NumCondR):-!,
condADestra(LeftProof,CondL),condADestra(RightProof,CondR),
NumCondR is 1+CondL+CondR.
condADestra(new_Tree(_,_,_,_,_,LeftProof,RightProof),NumCondR):-
condADestra(LeftProof,CondL),condADestra(RightProof,CondR),
NumCondR is CondL+CondR.
condASinistra(null,0).
condASinistra(new_Tree(_,condL,_,_,_,LeftProof,RightProof),NumCondL):-!,
condASinistra(LeftProof,CondL),condASinistra(RightProof,CondR),
NumCondL is 1+CondL+CondR.
condASinistra(new_Tree(_,_,_,_,_,LeftProof,RightProof),NumCondL):-
condASinistra(LeftProof,CondL),condASinistra(RightProof,CondR),
NumCondL is CondL+CondR.
nodiAlbero(null,0).
nodiAlbero(new_Tree(_,_,_,_,_,LeftProof,RightProof),Nodi):-nodiAlbero(LeftProof,NodiL),
nodiAlbero(RightProof,NodiR),Nodi is 1+NodiL+NodiR.
altezzaAlbero(null,0).
altezzaAlbero(new_Tree(_,_,_,_,_,LeftProof,RightProof),Heigth):-
altezzaAlbero(LeftProof,Left),altezzaAlbero(RightProof,Right),
massimo(Left,Right,Max),Heigth is 1+Max.
massimo(A,B,A):-A>B,!.
massimo(_,B,B).
etichetteUsate(JavaProof,NumEtichette):-elencoLabels(JavaProof,ListaLabels),
remove_duplicates(ListaLabels,ListaFinale),length(ListaFinale,NumEtichette).
elencoLabels(null,[]).
elencoLabels(new_Tree(Sequente,_,_,_,_,LeftProof,RightProof),ListaEtichette):-
elencoLabSequente(Sequente,ListaSeq),elencoLabels(LeftProof,LeftLab),
elencoLabels(RightProof,RightLab),append(ListaSeq,LeftLab,Temp),
append(Temp,RightLab,ListaEtichette).
elencoLabSequente([],[]).
elencoLabSequente([[X,_]|Tail],[X|TailLab]):-elencoLabSequente(Tail,TailLab).
elencoLabSequente([[X,_,Y]|Tail],[X,Y|TailLab]):-elencoLabSequente(Tail,TailLab).
elencoLabSequente([*|Tail],TailLab):-elencoLabSequente(Tail,TailLab).
lunghezzaSequente([],0).
lunghezzaSequente([[_,A]|Tail],Lung):-complessita(A,Compl),
lunghezzaSequente(Tail,LungTail),Lung is 2*Compl+LungTail.
lunghezzaSequente([[_,A,_]|Tail],Lung):-complessita(A,Compl),
lunghezzaSequente(Tail,LungTail),Lung is 1+2*Compl+LungTail.
complessita(neg A,Compl):-complessita(A,ComplResto),Compl is 1+ComplResto.
complessita(A and B,Compl):-complessita(A,ComplA),complessita(B,ComplB),
Compl is 1+ComplA+ComplB.
complessita(A or B,Compl):-complessita(A,ComplA),complessita(B,ComplB),
Compl is 1+ComplA+ComplB.
complessita(A -> B,Compl):-complessita(A,ComplA),complessita(B,ComplB),
Compl is 1+ComplA+ComplB.
complessita(A => B,Compl):-complessita(A,ComplA),complessita(B,ComplB),
Compl is 1+ComplA+ComplB.
complessita(_,1).
gradoSequente([],0).
gradoSequente([[_,A]|Tail],Grado):-grado(A,GrA),
gradoSequente(Tail,GradoTail),massimo(GrA,GradoTail,Grado).
gradoSequente([[_,A,_]|Tail],Grado):-grado(A,GrA),
gradoSequente(Tail,GradoTail),massimo(GrA,GradoTail,Grado).
grado(neg A,GrA):-grado(A,GrA).
grado(A and B,Grado):-grado(A,GrA),grado(B,GrB),massimo(GrA,GrB,Grado).
grado(A or B,Grado):-grado(A,GrA),grado(B,GrB),massimo(GrA,GrB,Grado).
grado(A -> B,Grado):-grado(A,GrA),grado(B,GrB),massimo(GrA,GrB,Grado).
grado(A => B,Grado):-grado(A,GrA),grado(B,GrB),massimo(GrA,GrB,Max),Grado is Max+1.
grado(_,0).
sequente(new_Tree(Sequente,_,_,_,_,_,_),Sequente).
regola(new_Tree(_,Rule,_,_,_,_,_),Rule).
antecedenteFormulaPrincipale(new_Tree(_,_,[Antec,_],_,_,_,_),Antec).
conseguenteFormulaPrincipale(new_Tree(_,_,[_,Conseg],_,_,_,_),Conseg).
antecedentePremessaSinistra(new_Tree(_,_,_,[Antec,_],_,_,_),Antec).
conseguentePremessaSinistra(new_Tree(_,_,_,[_,Conseg],_,_,_),Conseg).
antecedentePremessaDestra(new_Tree(_,_,_,_,[Antec,_],_,_),Antec).
conseguentePremessaDestra(new_Tree(_,_,_,_,[_,Conseg],_,_),Conseg).
alberoSinistro(new_Tree(_,_,_,_,_,Sinistro,_),Sinistro).
alberoDestro(new_Tree(_,_,_,_,_,_,Destro),Destro).
/* --------------------------------------------------------------------------------------- */
/* This predicate "destroies" the partition in a sequent */
appiattisci([Lit,Trans,Lab],Result):-append(Lit,Trans,Temp),
append(Temp,Lab,Result).
/* This predicate builds a proof tree used by the graphical interface */
/* Axioms */
costruisciJava(tree(falso),[Sigma,Delta],
new_Tree(Sequente,assioma,[[X,false],[]],[[],[]],[[],[]],null,null)):-
appiattisci(Sigma,Antecedente),
appiattisci(Delta,Conseguente),
member([X,false],Antecedente),
append(Antecedente,[*],Temp),
append(Temp,Conseguente,Sequente).
costruisciJava(tree(vero),[Sigma,Delta],
new_Tree(Sequente,assioma,[[],[X,true]],[[],[]],[[],[]],null,null)):-
appiattisci(Sigma,Antecedente),
appiattisci(Delta,Conseguente),
member([X,true],Conseguente),
append(Antecedente,[*],Temp),
append(Temp,Conseguente,Sequente).
costruisciJava(tree(assioma),[Sigma,Delta],
new_Tree(Sequente,assioma,[[F],[F]],[[],[]],[[],[]],null,null)):-
appiattisci(Sigma,Antecedente),
appiattisci(Delta,Conseguente),
member(F,Antecedente),member(F,Conseguente),
append(Antecedente,[*],Temp),
append(Temp,Conseguente,Sequente).
/* Rules */
/* and L */
costruisciJava(tree(andL,LeftProof,[X,A and B]),
[[LitSigma,TransSigma,ComplexSigma],Delta],
new_Tree(Sequente,andL,[[[X,A and B]],[]],[[[X,A],[X,B]],[]],[[],[]],JavaLeft,null)):-
appiattisci([LitSigma,TransSigma,ComplexSigma],Antecedente),
appiattisci(Delta,Conseguente),
append(Antecedente,[*],Temp),
append(Temp,Conseguente,Sequente),
delete(ComplexSigma,[X,A and B],ResComplexSigma),
put([X,A],LitSigma,ResComplexSigma,TempLitSigma,TempComplexSigma),
put([X,B],TempLitSigma,TempComplexSigma,NewLitSigma,NewComplexSigma),
costruisciJava(LeftProof,[[NewLitSigma,TransSigma,NewComplexSigma],Delta],JavaLeft).
/* or R */
costruisciJava(tree(orR,LeftProof,[X,A or B]),
[Sigma,[LitDelta,TransDelta,ComplexDelta]],
new_Tree(Sequente,orR,[[],[[X,A or B]]],[[],[[X,A],[X,B]]],[[],[]],JavaLeft,null)):-
appiattisci(Sigma,Antecedente),
appiattisci([LitDelta,TransDelta,ComplexDelta],Conseguente),
append(Antecedente,[*],Temp),
append(Temp,Conseguente,Sequente),
delete(ComplexDelta,[X,A or B],ResComplexDelta),
put([X,A],LitDelta,ResComplexDelta,TempLitDelta,TempComplexDelta),
put([X,B],TempLitDelta,TempComplexDelta,NewLitDelta,NewComplexDelta),
costruisciJava(LeftProof,[Sigma,[NewLitDelta,TransDelta,NewComplexDelta]],JavaLeft).
/* neg R */
costruisciJava(tree(negR,LeftProof,[X,neg A]),
[[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta]],
new_Tree(Sequente,negR,[[],[[X,neg A]]],[[[X,A]],[]],[[],[]],JavaLeft,null)):-
appiattisci([LitSigma,TransSigma,ComplexSigma],Antecedente),
appiattisci([LitDelta,TransDelta,ComplexDelta],Conseguente),
append(Antecedente,[*],Temp),
append(Temp,Conseguente,Sequente),
delete(ComplexDelta,[X,neg A],ResComplexDelta),
put([X,A],LitSigma,ComplexSigma,NewLitSigma,NewComplexSigma),
costruisciJava(LeftProof,[[NewLitSigma,TransSigma,NewComplexSigma],
[LitDelta,TransDelta,ResComplexDelta]],JavaLeft).
/* neg L */
costruisciJava(tree(negL,LeftProof,[X,neg A]),
[[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta]],
new_Tree(Sequente,negL,[[[X,neg A]],[]],[[],[[X,A]]],[[],[]],JavaLeft,null)):-
appiattisci([LitSigma,TransSigma,ComplexSigma],Antecedente),
appiattisci([LitDelta,TransDelta,ComplexDelta],Conseguente),
append(Antecedente,[*],Temp),
append(Temp,Conseguente,Sequente),
delete(ComplexSigma,[X,neg A],ResComplexSigma),
put([X,A],LitDelta,ComplexDelta,NewLitDelta,NewComplexDelta),
costruisciJava(LeftProof,[[LitSigma,TransSigma,ResComplexSigma],
[NewLitDelta,TransDelta,NewComplexDelta]],JavaLeft).
/* -> R */
costruisciJava(tree(impR,LeftProof,[X,A -> B]),
[[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta]],
new_Tree(Sequente,impR,[[],[[X,A -> B]]],[[[X,A]],[[X,B]]],[[],[]],JavaLeft,null)):-
appiattisci([LitSigma,TransSigma,ComplexSigma],Antecedente),
appiattisci([LitDelta,TransDelta,ComplexDelta],Conseguente),
append(Antecedente,[*],Temp),
append(Temp,Conseguente,Sequente),
delete(ComplexDelta,[X,A -> B],ResComplexDelta),
put([X,A],LitSigma,ComplexSigma,NewLitSigma,NewComplexSigma),
put([X,B],LitDelta,ResComplexDelta,NewLitDelta,NewComplexDelta),
costruisciJava(LeftProof,[[NewLitSigma,TransSigma,NewComplexSigma],
[NewLitDelta,TransDelta,NewComplexDelta]],JavaLeft).
/* => R */
costruisciJava(tree(condR,LeftProof,Y,[X,A => B]),
[[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta]],
new_Tree(Sequente,condR,[[],[[X,A => B]]],[[[X,A,Y]],[[Y,B]]],[[],[]],JavaLeft,null)):-
appiattisci([LitSigma,TransSigma,ComplexSigma],Antecedente),
appiattisci([LitDelta,TransDelta,ComplexDelta],Conseguente),
append(Antecedente,[*],Temp),
append(Temp,Conseguente,Sequente),
delete(ComplexDelta,[X,A => B],ResComplexDelta),
put([Y,B],LitDelta,ResComplexDelta,NewLitDelta,NewComplexDelta),
costruisciJava(LeftProof,[[LitSigma,[[X,A,Y]|TransSigma],ComplexSigma],
[NewLitDelta,TransDelta,NewComplexDelta]],JavaLeft).
/* and R */
costruisciJava(tree(andR,LeftProof,RightProof,[X,A and B]),
[Sigma,[LitDelta,TransDelta,ComplexDelta]],
new_Tree(Sequente,andR,[[],[[X,A and B]]],[[],[[X,A]]],[[],[[X,B]]],JavaLeft,JavaRight)):-
appiattisci(Sigma,Antecedente),
appiattisci([LitDelta,TransDelta,ComplexDelta],Conseguente),
append(Antecedente,[*],Temp),
append(Temp,Conseguente,Sequente),
delete(ComplexDelta,[X,A and B],ResComplexDelta),
put([X,A],LitDelta,ResComplexDelta,FirstLitDelta,FirstComplexDelta),
put([X,B],LitDelta,ResComplexDelta,SecLitDelta,SecComplexDelta),
costruisciJava(LeftProof,[Sigma,[FirstLitDelta,TransDelta,FirstComplexDelta]],JavaLeft),
costruisciJava(RightProof,[Sigma,[SecLitDelta,TransDelta,SecComplexDelta]],JavaRight).
/* or L */
costruisciJava(tree(orL,LeftProof,RightProof,[X,A or B]),
[[LitSigma,TransSigma,ComplexSigma],Delta],
new_Tree(Sequente,orL,[[[X,A or B]],[]],[[[X,A]],[]],[[[X,B]],[]],JavaLeft,JavaRight)):-
appiattisci([LitSigma,TransSigma,ComplexSigma],Antecedente),
appiattisci(Delta,Conseguente),
append(Antecedente,[*],Temp),
append(Temp,Conseguente,Sequente),
delete(ComplexSigma,[X,A or B],ResComplexSigma),
put([X,A],LitSigma,ResComplexSigma,FirstLitSigma,FirstComplexSigma),
put([X,B],LitSigma,ResComplexSigma,SecLitSigma,SecComplexSigma),
costruisciJava(LeftProof,[[FirstLitSigma,TransSigma,FirstComplexSigma],Delta],JavaLeft),
costruisciJava(RightProof,[[SecLitSigma,TransSigma,SecComplexSigma],Delta],JavaRight).
/* -> L */
costruisciJava(tree(impL,LeftProof,RightProof,[X,A -> B]),
[[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta]],
new_Tree(Sequente,impL,[[[X,A -> B]],[]],[[],[[X,A]]],[[[X,B]],[]],JavaLeft,JavaRight)):-
appiattisci([LitSigma,TransSigma,ComplexSigma],Antecedente),
appiattisci([LitDelta,TransDelta,ComplexDelta],Conseguente),
append(Antecedente,[*],Temp),
append(Temp,Conseguente,Sequente),
delete(ComplexSigma,[X,A -> B],ResComplexSigma),
put([X,A],LitDelta,ComplexDelta,NewLitDelta,NewComplexDelta),
put([X,B],LitSigma,ResComplexSigma,NewLitSigma,NewComplexSigma),
costruisciJava(LeftProof,[[LitSigma,TransSigma,ResComplexSigma],
[NewLitDelta,TransDelta,NewComplexDelta]],JavaLeft),
costruisciJava(RightProof,[[NewLitSigma,TransSigma,NewComplexSigma],
[LitDelta,TransDelta,ComplexDelta]],JavaRight).
/* => L */
costruisciJava(tree(condL,LeftProof,RightProof,Y,[X,A => B]),
[[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta]],
new_Tree(Sequente,condL,[[[X,A => B]],[]],[[],[[X,A,Y]]],[[[Y,B]],[]],JavaLeft,JavaRight)):-
appiattisci([LitSigma,TransSigma,ComplexSigma],Antecedente),
appiattisci([LitDelta,TransDelta,ComplexDelta],Conseguente),
append(Antecedente,[*],Temp),
append(Temp,Conseguente,Sequente),
put([Y,B],LitSigma,ComplexSigma,NewLitSigma,NewComplexSigma),
costruisciJava(RightProof,[[LitSigma,TransSigma,ComplexSigma],
[LitDelta,[[X,A,Y]|TransDelta],ComplexDelta]],JavaRight),
costruisciJava(LeftProof,[[NewLitSigma,TransSigma,NewComplexSigma],
[LitDelta,TransDelta,ComplexDelta]],JavaLeft).
/* EQ */
costruisciJava(tree(eq,LeftProof,RightProof,[X,A,Y],[X,B,Y]),
[[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta]],
new_Tree(Sequente,eq,[[[X,A,Y]],[[X,B,Y]]],[[[1,A]],[[1,B]]],
[[[1,B]],[[1,A]]],JavaLeft,JavaRight)):-
appiattisci([LitSigma,TransSigma,ComplexSigma],Antecedente),
appiattisci([LitDelta,TransDelta,ComplexDelta],Conseguente),
append(Antecedente,[*],Temp),
append(Temp,Conseguente,Sequente),
put([1,A],[],[],FirstLitSigma,FirstComplexSigma),
put([1,B],[],[],FirstLitDelta,FirstComplexDelta),
put([1,B],[],[],SecLitSigma,SecComplexSigma),
put([1,A],[],[],SecLitDelta,SecComplexDelta),
costruisciJava(LeftProof,[[FirstLitSigma,[],FirstComplexSigma],
[FirstLitDelta,[],FirstComplexDelta]],JavaLeft),
costruisciJava(RightProof,[[SecLitSigma,[],SecComplexSigma],
[SecLitDelta,[],SecComplexDelta]],JavaRight).
/* CS */
costruisciJava(tree(cs,LeftProof,RightProof,U,[X,A,Y]),
[[LitSigma,TransSigma,ComplexSigma],[LitDelta,TransDelta,ComplexDelta]],
new_Tree(Sequente,cs,[[[X,A,Y]],[]],[[],[[X,A]]],[[[U,A,U]],[]],JavaLeft,JavaRight)):-
appiattisci([LitSigma,TransSigma,ComplexSigma],Antecedente),
appiattisci([LitDelta,TransDelta,ComplexDelta],Conseguente),
append(Antecedente,[*],Temp),
append(Temp,Conseguente,Sequente),
member([X,A,Y],TransSigma),
put([X,A],LitDelta,ComplexDelta,NewLitDelta,NewComplexDelta),
costruisciJava(LeftProof,[[LitSigma,TransSigma,ComplexSigma],
[NewLitDelta,TransDelta,NewComplexDelta]],JavaLeft),
labelSubstitution(LitSigma,X,U,TempLitSigma),
labelSubstitution(TempLitSigma,Y,U,DefLitSigma),
labelSubstitution(TransSigma,X,U,TempTransSigma),
labelSubstitution(TempTransSigma,Y,U,DefTransSigma),
labelSubstitution(ComplexSigma,X,U,TempComplexSigma),
labelSubstitution(TempComplexSigma,Y,U,DefComplexSigma),
labelSubstitution(LitDelta,X,U,TempLitDelta),
labelSubstitution(TempLitDelta,Y,U,DefLitDelta),
labelSubstitution(TransDelta,X,U,TempTransDelta),
labelSubstitution(TempTransDelta,Y,U,DefTransDelta),
labelSubstitution(ComplexDelta,X,U,TempComplexDelta),
labelSubstitution(TempComplexDelta,Y,U,DefComplexDelta),
costruisciJava(RightProof,[[DefLitSigma,DefTransSigma,DefComplexSigma],
[DefLitDelta,DefTransDelta,DefComplexDelta]],JavaRight).